FDL - Nuprl Lemma : ma-interface-info_wf

Nuprl Lemma : ma-interface-info_wf

A:Type, I:MaInterface(A), i:Id.
(i

ma-interface-locs(I))

(

k:Knd.

(k

ma-interface-dom(I;i))

(ma-interface-info(I;i;k)

(V:Type

(State(ma-interface-ds(I;i))

V

(A + Top)))))

Definitions t T, x:A. B(x), Knd, b, {x:A| B(x)} , (x l), hasloc(k;i), x:AB(x), type List, S T, f(a), P Q, f(x), fpf-domain(f), x:A B(x), a:A fp B(a), Id, x. t(x), Type, State(ds), Top, left + right, P Q, P & Q, P Q, IdDeq, x.A(x), s = t, ma-interface-info(I;i;k), ma-interface-ds(I;i), MaInterface(T), ma-interface-locs(I), ma-interface-dom(I;i), {T}, SQType(T), s ~ t, False, A, A B, , , A c B, a < b, x:A. B(x)

Lemmas Knd sq, ma-interface-dom-hasloc, Id wf, id-deq wf, fpf wf, Knd wf, decl-state wf, top wf, fpf-ap wf, member-fpf-dom, fpf-trivial-subtype-top, assert wf, hasloc wf, l member wf